nLab primitive recursive arithmetic

Contents

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Mathematics

Contents

Idea

In proof theory, primitive recursive arithmetic, or PRA, is a finitist, quantifier-free formalization of the natural numbers.

PRA can express arithmetic propositions involving natural numbers and any primitive recursive function, including the operations of addition, multiplication, and exponentiation.

As a Skolem theory

Let TT be a Lawvere theory, i.e., a category with finite products TT equipped with a bijective-on-objects product-preserving functor X:Fin opTX: Fin^{op} \to T where FinFin is the category of finite cardinals and functions. Recall that a Skolem theory? is a Lawvere theory (T,X:Fin opT)(T, X: Fin^{op} \to T) in which N=X(1)N = X(1) carries a structure of parametrized natural numbers object in TT.

Abstractly, PRA can be described as the initial Skolem theory. Precise statements to this effect are difficult to pin down in the literature. (More later)

 References

For a dependent type theory conservative extension of primitive recursive arithmetic:

Last revised on September 19, 2024 at 23:18:38. See the history of this page for a list of all contributions to it.